Add influences of Boolean functions and the KKL theorem - #83

Formalize the influence lower bounds on the uniform hypercube {±1}^n:

- Influence/Martingale.lean: finite-average expectation, variance, entropy
  and Dirichlet form; the Doob martingale `condFirst` and its increments;
  orthogonal decompositions Var f = ∑ E[Δᵢ²] and 𝓔(f) = ∑ 𝓔(Δᵢ); the
  Bernoulli log-Sobolev inequality restated as Ent(f²) ≤ 2𝓔(f).
- Influence/Basic.lean: influences, Lemma 9.3, Theorem 9.4 (via the
  log-sum inequality), the bound 4 Var f · exp(-I/(2 Var f)) ≤ ∑ Iᵢ²,
  Theorem 9.5 (∑ Iᵢ² ≥ Var² log² n / n) and the KKL corollary
  `exists_influence_ge`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>